ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da).
ecl-halt(ds; da; x)  (event-info(ds;da) List)prop{i:l} 

latex

Definitions

top, t  T, Kind-deq, Knd, Type, x.A(x), x:A. B(x), x. t(x), fpf-cap(f; eq; x; z), decl-state(ds), x:A  B(x), <a, b>, event-info(ds;da), P  Q, False, A, A  B, , {x:A| B(x)} , , guard(T), sq_type(T), s = t, prop{i:l}, sqequal(s; t), left + right, x:AB(x), f(a), b, A c B, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , ma-valtype(da; k), #$n, a < b, void, spreadn(a; x,y,z.t(x;y;z)), subtype(S; T), ecl(ds; da), type List, l_exists(L; T; x.P(x)), P  Q, (x  l), P  Q, star-append(T; P; Q), iseg(T; l1; l2), x:A. B(x), append(as; bs), , l_all(L; T; x.P(x)), [], cons(car; cdr), x,y,z. t(x;y;z), x,y. t(x;y), x,y,z,w. t(x;y;z;w), ecl ind, ecl-halt(ds; da; x), Id, fpf(A; a.B(a))

Lemmas

fpf wf, Id wf, ecl ind wf, l all wf2, ma-valtype wf, bool wf, append wf, iseg wf, star-append wf, not wf, l member wf, l exists wf, event-info wf, nat wf, ecl wf, le wf, assert wf, Knd sq, subtype rel self, decl-state wf, fpf-cap wf, Knd wf, Kind-deq wf, top wf